Nuprl Lemma : filter_type
11,40
postcript
pdf
T
:Type,
P
:(
T
),
l
:(
T
List). filter(
P
;
l
)
({
x
:
T
|
(
P
(
x
))} List)
latex
Definitions
prop{i:l}
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
not
wf
,
bnot
wf
,
assert
wf
,
bool
wf
origin
T:Type, P:(T
), l:(T List). filter(P; l) 
({x:T| 
(P(x))} List) T:Type, P:(T), l:(T List). filter(P; l) ({x:T| (P(x))} List) Tx:A. B(x)